i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, v:T, ks:(Knd List),
tr:(k:{k:Knd| (k  ks)} State(ds)Valtype(da;k)TT).
((x  dom(ds)))
 (A:Realizer.
 R-Feasible(A)
  ((R-occurs(A;i;x)))
  ds || R-ds(A;i)
  da || R-da(A;i)
  (kks. (isrcv(k))  (R-da(A;source(lnk(k)))(k)?Void r Valtype(da;k)))
  (kks. k  dom(da))
  (k:Knd. (k  ks)  ((write-restricted(A;i;k))))
  (y:Id. (y  dom(ds  x : T))  ((read-restricted(A; i; y))))
  R-state-var-init(i;ds;da;x;T;v;ks;tr) || A) 

latex

Definitions

P & Q, R-state-var-init(i;ds;da;x;T;v;ks;tr), x. t(x), Top, , t  T, xL. P(x), Realizer, P  Q, a:A fp B(a), x:A. B(x), x(s)

Lemmas

not-R-occurs-init-compat, R-state-var-compat, R-compat-Rplus-sq, Id wf, id-deq wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, rationals wf, unit wf, R-Feasible wf, R-occurs wf, R-ds wf, Kind-deq wf, Knd wf, fpf-compatible wf, ma-valtype wf, lnk wf, lsrc wf, R-da wf, fpf-cap wf, isrcv wf, fpf-trivial-subtype-top, write-restricted wf, l member wf, read-restricted wf, not wf, fpf-single wf, top wf, fpf-join wf, fpf-dom wf, assert wf